block3 Circom を使ってゼロ知識証明のプログラムを書いてみよう

前回の復習

ゼロ知識証明とは？

命題が真であるということを、その命題が真であること以外の情報を明かさずに証明するプロトコル

zkSNARKs とは

Zero-Knowledge

秘密情報を明かさない

Succinct

証明のサイズは小さい

検証の時間は短い

Non-interactive

証明者と検証者の間でインタラクティブなやりとりを必要としない

Argument of knowledge

命題が真となる値を実際に「知っている」ことの証明

ある命題が真であることの証明

ある計算が正しく行われたことの証明

この考え方のシフトが重要

e.g.

h = sha256(m) となるような m を知っている

=> sha256(m)を正しく計算すると h になる

ゼロ知識証明では、プログラムのことを「回路」「Circuit」と表現されることが多い

電気回路のイメージから着想されている

Circom とは

ゼロ知識証明（zk-SNARKs）の構築に特化したプログラミング言語

ゼロ知識証明の構築から、証明の作成、検証用のスマートコントラクトの自動生成等、ゼロ知識証明を利用したプロダクトに必要な構成要素を用意してくれている

Circom で書いた回路をフロントエンドや Node.js で利用できるようにする便利ライブラリ

Trusted Setup の機能も提供している

Range Proof や Merkle Tree Inclusion Proof など、ゼロ知識証明でよく使われる実装がまとまっている公式ライブラリ

特徴

プログラミングのメンタルモデルが結構違う...

ある計算において適切な input がある場合にその計算が正しく行われることを制約付けるプログラムを書くこと

ロジックを書くというよりも、そのロジックが正しく動くことを制約するプログラムを書く、みたいな感じ？

e.g

h = sha256(m)

m を input とした時 sha256 が正しく計算され、 h がアウトプットされると制約するプログラムを書く

「sha256 のプログラムを書く」ではなく「正しく sha256 されることを制約するプログラムを書く」

様々な制約を実装する際、それらをすべて Linear Expression（線形式）とQuadratic Expression（2次方程式）で表現する必要があります。if 文や switch 文などは制約を作る際に利用できません。（通常の処理では利用可能です）

e.g.

Linear Expression（線形式）

$ 2x + 3y + 2

Quadratic Expression（2次式）

$ (2x + 3y + 2) \times (x + y) + 6x + y - 2

有限体上で計算が行われている

ゼロ知識証明において求められる数学的な要件

演算の数の少なさ

計算の実行時間の短さ

暗号学的な安全性

有限体上の計算は

特定の範囲内に制限される

実行時間が比較的に短い

楕円曲線暗号など、暗号プリミティブを利用できる

他にも様々な特徴がありますが、詳しくはドキュメントを読んでください。

使い方の流れ

https://gblobscdn.gitbook.com/assets%2F-MDt-cjMfCLyy351MraT%2F-ME35kSLplV3Z39JJsLE%2F-ME37Q2MlDc67k0-jzQS%2Fcircomsnarkjs.png?alt=media&token=4b1b1c11-a1d4-4048-8c3a-0c7b02f4930a

コードを書く前にエクササイズ！

code:q1.txt

1. condition という変数があり、そこには 1 か 0 かが代入されています。

2. result という何も代入されていない変数を用意します。

3. condition に 1 が入っている場合は result に 3 を、0 が入っている場合には result に 4 を代入するプログラムを、三項演算子、if 文、switch 文等を使わずに、 Linear Expression（線形式）や Quadratic Expression（2次方程式）の考え方を参考しながら実装する擬似コードをかいてください。

code:a1.ts

let condition // 1 or 0

let result

result = 3 * (condition) + 4 * (1 - condition)

ChatGPT 先生の回答

code:ChatGPT先生のこたえ

以下は、線形式を用いて、条件に基づいて結果を代入するプログラムの擬似コードです。

result = 4 + (condition - 1) * (3 - 4)

この式は、condition が 1 の場合には (condition - 1) が 0 となり、result に 4 が代入されます。一方、condition が 0 の場合には (condition - 1) が -1 となり、(3 - 4) が -1 となり、result に 4 + (-1) = 3 が代入されます。

たぶん以下だと work する

result = 4 + condition * (3 - 4)

zkrepl を使ってコード書いてみよう！

ブラウザ上で Circom のコードを書いてコンパイルできるサービスです

軽く説明

template

Circom で算術回路を書く時に宣言する予約語

そのスコープ内に様々なロジックを記述していく

component

template をインスタンス化する時に使う予約語

関数を定義してるだけのようなイメージ

それを外部から include することができる

あとで circomlib にあるファイルをみてみよう！

signal

算術回路に渡される引数のようなもの

public / private を設定できる。

default は private

INPUT

zkrepl 独自もの

input を定義し、証明を生成する際等に利用される

Example 1

c = example(a, b) が正しく計算されることを制約づけるプログラム

パラメータ

public input a と private input b

計算内容

c = 4 * a + 2 * b - 42

出力値

c

code:example1.circom

pragma circom 2.1.2;

template Example () {

signal input a;

signal input b;

signal output c;

// public input a と private input b を使って下記計算が正しく行われ c がアウトプットされると制約づける

c <== 4 * a + 2 * b - 42;

}

/* INPUT = {

"a": "5",

"b": "11"

} */

エクササイズ2

code:q2.txt

下のドキュメントを読み、上のコードに1行追加して c が 0 であるという制約を付与してください。

code:a2.txt

エクササイズ3

code:q3.txt

code:a3.circom

pragma circom 2.1.2;

include "circomlib/comparators.circom";

template Example () {

signal input a;

signal input b;

signal output c;

component isZero = IsZero();

isZero.in <== 4 * a + 2 * b - 42;

}

/* INPUT = {

"a": "5",

"b": "11"

} */

エクササイズ4

code:q4.txt

下のライブラリのとある template を利用し、public input a よりも、private input b が大きいという制約をつけるプログラムを書いてください。

code:a3.circom

もっと勉強したい人